T:Type, a, b, c:T List. l_disjoint(T;b @ c;a)  l_disjoint(T;b;a) & l_disjoint(T;c;a) 

latex

Definitions	(x  l), P & Q, P  Q, False, A, P  Q, x:A. B(x), t  T, Prop, P  Q, P  Q, as @ bs, x. t(x), l_disjoint(T;l1;l2), {T}
Lemmas	iff functionality wrt iff, all functionality wrt iff, not functionality wrt iff, and functionality wrt iff, member append, iff wf, append wf, not wf, l member wf